(set-logic UFNRA)
(set-option :proof true)
(set-option :smt.arith.solver 6)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const r1 Real)
(declare-const r3 Real)
(declare-const r5 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const r11 Real)
(declare-const r14 Real)
(declare-const r15 Real)
(declare-const r16 Real)
(declare-const r18 Real)
(declare-sort S0 0)
(declare-const S0-0 S0)
(declare-const v18 Bool)
(declare-const r19 Real)
(declare-const v19 Bool)
(declare-const v20 Bool)
(push 1)
(declare-sort S1 0)
(assert (exists ((q0 S1)) v19))
(push 1)
(declare-const v21 Bool)
(declare-const v22 Bool)
(push 1)
(declare-const v23 Bool)
(assert (exists ((q1 Bool)) (not (xor v9 (not (> 814408.0 0.447 r18 814408.0 r14))))))
(declare-const v24 Bool)
(push 1)
(declare-const v25 Bool)
(declare-const v26 Bool)
(push 1)
(declare-const S0-1 S0)
(declare-sort S2 0)
(declare-const v27 Bool)
(declare-const r20 Real)
(assert (forall ((q2 S1) (q3 S2) (q4 S2)) (not (distinct q4 q4))))
(declare-sort S3 0)
(declare-const S3-0 S3)
(declare-const v28 Bool)
(declare-const r21 Real)
(declare-const v29 Bool)
(declare-sort S4 0)
(declare-const v30 Bool)
(declare-const S0-2 S0)
(declare-const S2-0 S2)
(declare-const v31 Bool)
(pop 1)
(declare-const v32 Bool)
(declare-const r22 Real)
(pop 1)
(declare-const v33 Bool)
(declare-const S1-0 S1)
(push 1)
(declare-const v34 Bool)
(declare-const r23 Real)
(declare-const v35 Bool)
(declare-const v36 Bool)
(pop 1)
(declare-const v37 Bool)
(declare-const v38 Bool)
(declare-const v39 Bool)
(declare-const v40 Bool)
(declare-const r24 Real)
(declare-const v41 Bool)
(assert (forall ((q5 Real) (q6 S1) (q7 Bool) (q8 S1)) (> r1 0.5406 837636664.0 53064803.0 4745.0)))
(declare-const v42 Bool)
(declare-const v43 Bool)
(declare-const r25 Real)
(assert (forall ((q9 Real) (q10 S0) (q11 S1)) (not (>= 950.0 r25))))
(pop 1)
(declare-const v44 Bool)
(assert (forall ((q12 S0) (q13 S1) (q14 Bool)) (not v19)))
(declare-const r26 Real)
(declare-const S0-1 S0)
(declare-const v45 Bool)
(declare-sort S2 0)
(declare-const v46 Bool)
(declare-const r27 Real)
(declare-const v47 Bool)
(push 1)
(declare-const v48 Bool)
(declare-const r28 Real)
(declare-const v49 Bool)
(declare-const r29 Real)
(pop 1)
(pop 1)
(declare-const r30 Real)
(declare-const v50 Bool)
(assert (forall ((q15 S0) (q16 S0) (q17 Real)) v0))
(declare-const v51 Bool)
(declare-const S1-0 S1)
(declare-const v52 Bool)
(declare-const S1-1 S1)
(declare-const v53 Bool)
(declare-const v54 Bool)
(pop 1)
(declare-const v55 Bool)
(declare-const v56 Bool)
(declare-const v57 Bool)
(push 1)
(declare-const S0-1 S0)
(declare-const r31 Real)
(declare-const r32 Real)
(push 1)
(declare-const r33 Real)
(declare-const v58 Bool)
(declare-const v59 Bool)
(push 1)
(push 1)
(declare-sort S1 0)
(declare-const v60 Bool)
(declare-const r34 Real)
(declare-const v61 Bool)
(declare-const v62 Bool)
(pop 1)
(declare-const S0-2 S0)
(declare-const r35 Real)
(declare-const v63 Bool)
(declare-const r36 Real)
(declare-const v64 Bool)
(declare-const v65 Bool)
(declare-const v66 Bool)
(declare-const r37 Real)
(declare-const v67 Bool)
(push 1)
(push 1)
(declare-sort S1 0)
(declare-const v68 Bool)
(declare-const v69 Bool)
(pop 1)
(declare-const v70 Bool)
(push 1)
(declare-const S0-3 S0)
(push 1)
(declare-const S0-4 S0)
(declare-const v71 Bool)
(pop 1)
(declare-const v72 Bool)
(declare-sort S1 0)
(push 1)
(declare-const v73 Bool)
(declare-sort S2 0)
(declare-const v74 Bool)
(pop 1)
(push 1)
(declare-const S1-0 S1)
(assert (exists ((q18 S1) (q19 Real)) (not (= q18 q18 q18 q18))))
(declare-const r38 Real)
(pop 1)
(declare-const v75 Bool)
(declare-const v76 Bool)
(declare-const r39 Real)
(declare-const v77 Bool)
(declare-const v78 Bool)
(assert (exists ((q20 S0) (q21 Bool) (q22 Bool) (q23 S1)) (not (= q23 q23 q23 q23 q23))))
(declare-const S0-4 S0)
(declare-const r40 Real)
(declare-const v79 Bool)
(declare-const v80 Bool)
(push 1)
(declare-const v81 Bool)
(declare-const v82 Bool)
(declare-const v83 Bool)
(declare-const v84 Bool)
(declare-const r41 Real)
(declare-const v85 Bool)
(push 1)
(declare-const v86 Bool)
(declare-const S0-5 S0)
(declare-const r42 Real)
(declare-const v87 Bool)
(declare-const r43 Real)
(pop 1)
(declare-const r44 Real)
(declare-const v88 Bool)
(pop 1)
(declare-const r45 Real)
(declare-const r46 Real)
(pop 1)
(declare-const r47 Real)
(declare-const v89 Bool)
(push 1)
(declare-const v90 Bool)
(declare-const v91 Bool)
(assert (exists ((q24 Bool) (q25 Bool) (q26 Bool)) (not (and (>= r5 4745.0) v70 q26 v20 q24))))
(declare-const v92 Bool)
(assert (exists ((q27 S0) (q28 Real)) v91))
(push 1)
(declare-const S0-3 S0)
(declare-const v93 Bool)
(assert (forall ((q29 Real) (q30 Bool) (q31 Bool) (q32 Bool)) (=> (= q29 q29 q29 q29) (= q30 v5 v55 q30 v9 q31 v13 v63))))
(pop 1)
(declare-const v94 Bool)
(push 1)
(declare-const r48 Real)
(declare-const v95 Bool)
(declare-const r49 Real)
(push 1)
(declare-sort S1 0)
(push 1)
(declare-const v96 Bool)
(declare-const v97 Bool)
(declare-const v98 Bool)
(push 1)
(pop 1)
(declare-const v99 Bool)
(push 1)
(declare-const r50 Real)
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958)))
(assert (or (< r10 528404.958) v5 v63 v5))
(assert (or v5))
(assert (or v5 (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14)) v5 v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63))
(assert (or (= (- r9) r18)))
(assert (or (= (- r9) r18) (< r10 528404.958)))
(assert (or v63))
(assert (or (= (- r9) r18) (= (- r9) r18) (< r10 528404.958)))
(assert (or (= (- r9) r18) v5 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v63))
(assert (or (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v63))
(assert (or (< r10 528404.958) (< r10 528404.958) v5))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5 v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63))
(assert (or (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v63 (< r10 528404.958) (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) v5))
(assert (or v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63 v63))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5))
(assert (or (= (- r9) r18) (= (- r9) r18)))
(assert (or (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) v5))
(assert (or v63 (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958) v5))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) (= (- r9) r18)))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18)))
(assert (or (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (= (- r9) r18) v63 v5 (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) (< r10 528404.958)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14)) v5))
(assert (or (< r10 528404.958)))
(assert (or (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) (= (- r9) r18)))
(assert (or v63 (= (- r9) r18) (= (- r9) r18) (< r10 528404.958)))
(assert (or (= (- r9) r18)))
(assert (or (< r10 528404.958)))
(assert (or v63 v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v5 (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958)))
(assert (or v63 (< r10 528404.958) v63 (< r10 528404.958) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14)) v63))
(assert (or v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5))
(assert (or (= (- r9) r18) (< r10 528404.958) v63 (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (< r10 528404.958) (= (- r9) r18) (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14)) v63 v5 v63 (= (- r9) r18) (= (- r9) r18)))
(assert (or v5 (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14)) v63 (= (- r9) r18)))
(assert (or (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v5))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) v5 (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5 v5))
(assert (or (= (- r9) r18) (= (- r9) r18) v63 v5 v63 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63 (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) v5 (= (- r9) r18) (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) v63 (< r10 528404.958) (< r10 528404.958) v5 (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958)))
(assert (or v63 v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (= (- r9) r18)))
(assert (or (= (- r9) r18)))
(assert (or (< r10 528404.958)))
(assert (or v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (= (- r9) r18) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (= (- r9) r18)))
(assert (or (< r10 528404.958) (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958) v5 v63 v5))
(assert (or v63 v63 (not (> 814408.0 0.447 r18 814408.0 r14)) v63))
(assert (or v5 (< r10 528404.958)))
(assert (or (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5 (< r10 528404.958)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v63 (= (- r9) r18) v5))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v63 (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18)))
(assert (or v63 (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958)))
(assert (or (= (- r9) r18) v63 (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958)))
(assert (or (= (- r9) r18) v63 (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958)))
(assert (or v5 (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) v5))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) v5 (< r10 528404.958)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) v63 (< r10 528404.958) v63 v63))
(assert (or (= (- r9) r18)))
(assert (or (< r10 528404.958) v63))
(assert (or (= (- r9) r18)))
(assert (or (= (- r9) r18) (= (- r9) r18)))
(assert (or v63 (< r10 528404.958) v63 (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14)) v63 v63 v5 v5 (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14)) v5 (< r10 528404.958)))
(assert (or v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63 (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63 (= (- r9) r18)))
(assert (or v63))
(assert (or v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18)))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v63 (= (- r9) r18) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) v63 v63 (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5))
(assert (or (= (- r9) r18) v5))
(assert (or (< r10 528404.958) v63 (= (- r9) r18)))
(assert (or (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (< r10 528404.958) v5))
(assert (or v63))
(assert (or v63 (= (- r9) r18) (< r10 528404.958)))
(assert (or v5 v63 (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5 (< r10 528404.958) v63 (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) v63))
(assert (or (= (- r9) r18) v63 v63 (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (= (- r9) r18)))
(assert (or (= (- r9) r18) (< r10 528404.958) v5 v5))
(assert (or v63))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) v63 (= (- r9) r18) (< r10 528404.958) v63 v63 v63 v5 (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) (< r10 528404.958) v63 (< r10 528404.958) v5 (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958)))
(assert (or v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v5 v63 v63 (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) v63 (not (> 814408.0 0.447 r18 814408.0 r14)) v5 (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v5 (< r10 528404.958)))
(assert (or (= (- r9) r18)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958)))
(assert (or (< r10 528404.958) (< r10 528404.958)))
(assert (or (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958)))
(assert (or (= (- r9) r18)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) (= (- r9) r18)))
(assert (or (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63 v5 (< r10 528404.958) v63 (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v63 (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v63))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v63))
(assert (or (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18)))
(assert (or v63))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (= (- r9) r18)))
(assert (or (< r10 528404.958)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5 (= (- r9) r18)))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18)))
(assert (or v63 v63 v5))
(assert (or v63 v5 (< r10 528404.958)))
(assert (or (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958) (= (- r9) r18) (< r10 528404.958)))
(assert (or v5 v63))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5 (< r10 528404.958) v5 (= (- r9) r18) v5))
(assert (or (< r10 528404.958)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958)))
(assert (or (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63))
(assert (or (< r10 528404.958) v63))
(assert (or v5))
(assert (or (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) v63 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5))
(assert (or v63))
(assert (or v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (< r10 528404.958) (= (- r9) r18)))
(assert (or (< r10 528404.958) v5 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5 v63))
(assert (or v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (= (- r9) r18)))
(assert (or v5 v63 v63))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (< r10 528404.958)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (< r10 528404.958) (= (- r9) r18) v63 (< r10 528404.958) (= (- r9) r18) v63 v63))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) v63 (= (- r9) r18)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18) (= (- r9) r18) v5))
(assert (or v5))
(assert (or (< r10 528404.958) v5 v63 (not (> 814408.0 0.447 r18 814408.0 r14)) v5))
(assert (or (= (- r9) r18) (< r10 528404.958)))
(assert (or (= (- r9) r18) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958)))
(assert (or v5))
(assert (or (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (= (- r9) r18) (= (- r9) r18) (= (- r9) r18) v5 v63))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (< r10 528404.958) (= (- r9) r18)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (< r10 528404.958)))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5))
(assert (or v63 (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (= (- r9) r18) (= (- r9) r18)))
(assert (or v63))
(assert (or v63 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958) v63 (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v63))
(assert (or (< r10 528404.958)))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5 (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v5 v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v63 (= (- r9) r18) (< r10 528404.958) v5))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or v5))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (= (- r9) r18)))
(assert (or v63))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (= (- r9) r18)))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5))
(assert (or v5))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5 (< r10 528404.958) (< r10 528404.958) v63))
(assert (or v5))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (= (- r9) r18) (= (- r9) r18)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (< r10 528404.958) v5 v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5 v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63))
(assert (or (= (- r9) r18) v63))
(assert (or v63 (< r10 528404.958) (= (- r9) r18)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) v63 (= (- r9) r18) v63 v63 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v63 (= (- r9) r18)))
(assert (or (< r10 528404.958) v63 (not (> 814408.0 0.447 r18 814408.0 r14)) v5))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958) (= (- r9) r18) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (< r10 528404.958)))
(assert (or (= (- r9) r18) (< r10 528404.958) (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (= (- r9) r18)))
(assert (or (< r10 528404.958) (< r10 528404.958) v5))
(assert (or (< r10 528404.958)))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v63 v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (= (- r9) r18) v5 v63))
(assert (or v63 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5))
(assert (or v5))
(assert (or v63 (not (> 814408.0 0.447 r18 814408.0 r14)) v63 (not (> 814408.0 0.447 r18 814408.0 r14)) v63))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5 (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5))
(assert (or v5 (< r10 528404.958) v5 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (< r10 528404.958)))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (< r10 528404.958)))
(assert (or (= (- r9) r18)))
(assert (or v5))
(assert (or v5))
(assert (or v63))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14)) v5 (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or v5))
(assert (or v5 (= (- r9) r18) (= (- r9) r18) (< r10 528404.958) (= (- r9) r18) (< r10 528404.958)))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (< r10 528404.958) v63))
(assert (or (= (- r9) r18) (= (- r9) r18)))
(assert (or v63))
(assert (or (not (> 814408.0 0.447 r18 814408.0 r14)) (= (- r9) r18)))
(assert (or v63 v63))
(assert (or v5 (< r10 528404.958)))
(assert (or (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) v5))
(assert (or v63))
(assert (or (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0)))))
(assert (or (< r10 528404.958) (<= 48029542.0 (* 843.92 r1 (* 97.0 r1 814408.0 97.0))) (not (> 814408.0 0.447 r18 814408.0 r14)) (not (> 814408.0 0.447 r18 814408.0 r14))))
(assert (or (< r10 528404.958)))
(check-sat)
(exit)
